T:Type{i}, eq:EqDecider(T), d:a:T fp Type{i}. atom-free-decl{i:l}(T; eq; d)  Prop{i'} 

latex

Definitions	Type, t  T, x:A. B(x), EqDecider(T), x. t(x), a:A fp B(a), x.A(x), Top, x:AB(x), x  dom(f), b, {x:A| B(x) }, AtomFree(T;x), x,y. t(x;y), xdom(f). v=f(x)   P(x;v), AtomFree(d)
Lemmas	fpf-all wf, atom-free wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, deq wf